TITOLO ASSEGNO: Semantica Differenziale di Programmi.

PROGETTO DI RICERCA.

Il Dottore di Ricerca selezionato dovrà occuparsi di studiare la semantica differenziale dei linguaggi di programmazione funzionale con effetti. Più nello specifico, ci si concentrerà sullo studio delle relazioni logiche, della coinduzione, della semantica a giochi e della logica lineare differenziale. Tutte queste aree della semantica sono state ampiamente studiate in un quadro qualitativo, in cui il risultato del confronto tra programmi diversi è tipicamente un valore booleano, tramite il quale è possibile concludere se i programmi in questione siano o meno confrontabili. Quello che ci si propone di fare è generalizzare tali quadri semantici in senso quantitativo, rendendoli in grado di determinare la distanza tra tali programmi, misurata tramite un valore non necessariamente numerico. Questo assegno di ricerca è finanziato dall’ERC Consolidator Grant DIAPASoN - DLV-818616.

Piano DI ATTIVITA'.

Il Dottore di Ricerca selezionato si occuperanno nei ventiquattro mesi dell’assegno di:
- Generalizzare le logiche relazionali differenziali a calcoli con ricorsione all'ordine superiore ed effetti.
- Introdurre una nozione di distanza comportamentale, estensione conservativa delle metriche comportamentali, che permetta di tener traccia non solo di un limite superiore alle distanze visibili, ma anche del loro effettivo valore.
- Analizzare la semantica dei giochi, e in particolare la sua capacità di determinare la distanza tra programmi, con particolare riferimento all'intrinseca simmetria di tale quadro semantico.
- Studiare in che senso la logica differenziale permetta di valutare il grado di sensitività dei programmi.

      ----------------------------------------

TITLE: Differential Program Semantics.

RESEARCH PROJECT.

The selected PhD will study the differential semantics of impure functional programming languages ​. More specifically, the focus will be on the study of logical relations, coinduction, game semantics, and differential linear logic. All these areas of program semantics have been extensively studied in a qualitative framework, where the result of the comparison between distinct programs is typically a Boolean value, through which it is possible to conclude whether or not the programs in question are comparable. What we propose to do is to generalise these semantic frameworks in a quantitative sense, making them able to determine the distance between these programs, measured by a non-necessarily numerical value. This research is funded by the ERC Consolidator Grant DIAPASoN - DLV-818616.

ACTIVITY PLAN.

The selected PhD will be involved in one or more of the following tasks:
- Generalise differential logical relations to calculi featuring higher order recursion and effects.
- Introduce a new notion of behavioural distance, as a conservative extension of behavioural metrics, which allows to keep track not only of an upper bound on the visible distances, but also of their actual value.
- Analyse the semantics of games, and in particular their ability to determine the distance between programs, with particular emphasis to the intrinsic symmetry of this semantic framework.
- Study in which sense differential linear logic allows to evaluate the degree of sensitivity of functional programs.